the_w:World. E  Type 

latex

Definitions	E, A, b, isnull(a), 1of(t), a(i;t), 2of(t), , Id, x. t(x), x:A. B(x), t  T, World
Lemmas	world wf, pi2 wf, w-a wf, pi1 wf, w-isnull wf, assert wf, not wf, nat wf, Id wf